(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(declare-fun u () Real)
(declare-fun v () Real)
(declare-fun w () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun aa () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun af () Real)
(declare-fun ag () Real)
(declare-fun ah () Real)
(declare-fun ai () Real)
(declare-fun aj () Real)
(declare-fun ak () Real)
(declare-fun al () Real)
(declare-fun am () Real)
(declare-fun an () Real)
(declare-fun ao () Real)
(declare-fun ap () Real)
(declare-fun aq () Real)
(declare-fun ar () Real)
(declare-fun at () Real)
(declare-fun au () Real)
(declare-fun av () Real)
(declare-fun aw () Real)
(assert (forall ((x Real)) (or (<= 0.0 v) (and (=> (or (< 0.0 x) (>= x v)) (and (or (and (<= 0.0 (/ 54 m al)) (> (/ 60 m al) ac) (< 0.0 (+ c (* g v)))) (<= (- 4 c (/ 183 g v)) ac)) (>= x ae))) (= (* 67 e (* 154 g v)) 2.0)) (= aw (+ aa al)) (and (or (and (or (and (= ac q) (= (+ m al) 4)) (= t 0.0)) (= t 2.0) (= u 2.0) (> (* y (- (/ 232 n n) (- (/ 19 ap (+ 64 f t))))) w) (> 0.0 n ac) (<= ac (/ 245 b (/ 7 f t)))) (< 0.0 ac)) (< 0.0 ae)))))
(assert (or (and (or (and (or (and (< 0.0 (+ (* (- ak) ai) (/ 85 b o))) (<= (+ ai (* b o)) (* j x)) (>= 0.0 ai ar)) (> 0.0 ar)) (= (+ 89 e s) 0)) (<= o 53) (> (* b o) (/ 214 j x))) (= (+ aa af) 2.0) (<= (- (/ 63 k z) (- (- (/ 137 a n) (/ 21 a n) ak))) ah) (<= 0.0 ak) (> 0.0 (+ 249 a)) (< (* a n) (* j x)) (<= 0.0 (* d q)) (< 0.0 (* j x))) (<= 0 (* j x))))
(assert (= a (+ n am)))
(assert (= b (+ 3 o aq)))
(assert (= c (* p ao)))
(assert (= d (* q aj aq r ai)))
(assert (= e (+ s ao)))
(assert (= f (/ 207 t aq)))
(assert (= at (+ u am)))
(assert (= g (+ 182 v ao)))
(assert (= h (/ 17 ab aj)))
(assert (= i (* w aj)))
(assert (= j (+ x an)))
(assert (= au (/ 119 y al)))
(assert (= k (+ z aw ac)))
(assert (= l (/ 9 ad ai)))
(assert (= av (/ ae ak)))
(assert (= aa (- af al)))
(assert (= m (/ 0 ag al)))
(check-sat)
